sig Avaliacao{
	nota : set Nota
}


sig ProvaOral{
	docentes : set Docente
}


sig PlanoCurso{
	creditos : some ECTS
}


sig Periodo{
	data_inicio : one Data,
	data_fim : one Data,
	local : one Local
}


sig AplicacaoTutoria{
	fichas_disponiveis : set Ficha,
	sumarios : Sumario -> Aula,
	materiais_aulas : Aula -> some Material
}


sig Curso{
	plano : one PlanoCurso,
	regime : one Regime
}


sig Aula{}


sig EspecializacaoTEC extends Curso{}


sig CotacaoMultipla extends Cotacao{
	correcta : one CotacaoNota,
	incorrecta : one CotacaoNota,
	omissao : one CotacaoNota

}


sig Dia{}


sig Data{
	dia : one Dia,
	mes : one Mes,
	ano : one Ano,
	hora : one Hora
}


sig Regime{}


sig ResumoDesc{}


sig Director{}


sig Precedencia{}


sig Relatorio{
	analise_resultados : one AnaliseResultado,
	sugestoes : set Sugestao
}


sig MestradoInt extends Curso{}


sig Mes{}


sig ConselhoCientifico{}


sig Nocturno extends Regime{}


sig CompetenciaProgramatica{}


sig Juri{}


sig CotacaoNormal extends Cotacao{
	cotacao : one CotacaoNota
}


sig Sugestao{}


sig FormatoEnunciado{}


sig Sumario{}


sig EscolhaMultipla extends FormatoEnunciado{}


sig Docente{}


sig EnunciadosProvas{
	tempo_maximo : one Tempo,
	cotacao_maxima : Questao -> Cotacao
}


sig CotacaoNota{}


sig Aluno{
	matriculado : Ano -> one Curso,
	inscricoes : UnidadeCurricular -> some ECTS,
	inscricoes_passadas : some UnidadeCurricular,
	aprovado: set UnidadeCurricular,
	avaliacao: UnidadeCurricular -> Avaliacao,
	provas: UnidadeCurricular -> some ProvaAvaliacao
}


sig ECTS{}


sig ConteudoFicha{}


sig AnaliseResultado{}


sig Material{}


sig ConselhoPedagogico{
	relatorios : set Relatorio
}


sig Ano{}


sig Questao{}


sig MetodoEnsino{}


sig Hora{}


sig OrgaoCompetente{
	fichas : set Ficha
}


sig Local{}


sig UnidadeOrganica{
	conselho : one ConselhoCientifico,
	ocompetente : one OrgaoCompetente,
	director : one Director
}


sig EnunciadoProvas{
	formato: one FormatoEnunciado,
	tempo_maximo : one Tempo,
	cotacao_maxima : Questao -> Cotacao
}


sig ProvaAvaliacao{
	enunciado : one EnunciadoProvas,
	data_realizacao : one Data,
	periodo_consulta : one Periodo,
	juri : lone Juri
}


sig Bibliografia{}


sig Curso1Ciclo extends Curso{}


sig Ficha{
	horas_contacto  : some Hora,	
	resumo : one ResumoDesc,
	precedencias : set UnidadeCurricular,
	competencia_progr : some CompetenciaProgramatica,
	metodos_ensino : some MetodoEnsino,
	bibliografia_basica: some Bibliografia
}


sig Tempo{}


sig UnidadeCurricular{
	responsavel: lone Docente,
	ficha_funcionamento: responsavel -> one Ficha
}


sig Nota{}


sig Cotacao{}


pred MarcaDatasAvaliacao[d:Director, p,p':ProvaAvaliacao, data:Data, periodo:Periodo]{
	p'.enunciado = p.enunciado
	p'.data_realizacao = data
	p'.periodo_consulta = periodo
}


pred DisponibilizaOnline [d:Docente,u:UnidadeCurricular, a,a':AplicacaoTutoria]{
	d = u.responsavel
	a.fichas_disponiveis in a'.fichas_disponiveis
	//Quest�o t�cnica - IsoMorfismo
	one ficha: a'.fichas_disponiveis |{
		ficha.horas_contacto = ~(u.ficha_funcionamento).d.horas_contacto &&
		ficha.resumo = ~(u.ficha_funcionamento).d.resumo &&
		ficha.precedencias = ~(u.ficha_funcionamento).d.precedencias &&
		ficha.competencia_progr = ~(u.ficha_funcionamento).d.competencia_progr &&
		ficha.metodos_ensino = ~(u.ficha_funcionamento).d.metodos_ensino &&
		ficha.bibliografia_basica = ~(u.ficha_funcionamento).d.bibliografia_basica
	}
	#(a'.fichas_disponiveis)=#(a.fichas_disponiveis)+1
}


pred AvaliacaoInv[a:Avaliacao]{
	#(a.nota)>=0 && #(a.nota)<=20
}


pred InvEnunciado[e:EnunciadoProvas]{
	e.formato=EscolhaMultipla => ~(e.cotacao_maxima).Questao = CotacaoMultipla
}


pred Avaliacao[u:UnidadeCurricular, a,a':Aluno, av:Avaliacao, d:Docente]{
	//O docente tem que ser respons�vel da unidade curricular
	u.responsavel = d
	a'.matriculado = a.matriculado
	a'.inscricoes = a.inscricoes
	a'.inscricoes_passadas = a.inscricoes_passadas
	a'.aprovado = a.aprovado
	a'.avaliacao = a.avaliacao + (u->av)
}


pred InvProvasAvaliacaoAlunos[a: Aluno]{
	a.provas.ProvaAvaliacao in a.inscricoes.ECTS
}


pred Inv[a: Aluno]{
	ECTSAnuais[a]
	AprovadoInscrito[a]
	(~(a.matriculado.regime).Ano = Nocturno) => ECTSNocturno[a]
	AprovacaoCorrecta[a]
	InvProvasAvaliacaoAlunos[a]
}


pred DistribuicaoServicoDocente[c:ConselhoCientifico, d:Docente, u,u':UnidadeCurricular]{
	u'.responsavel = d
}


pred ECTSNocturno[a: Aluno]{
	#(~(a.inscricoes).(UnidadeCurricular - a.inscricoes_passadas))<=#(a.matriculado.plano.creditos)
	#(~(a.inscricoes).(a.inscricoes_passadas))<=18
}


pred TransitAno[a,a':Aluno]{
	#~(a.inscricoes).(UnidadeCurricular-a.aprovado) <=24
}


pred DocenteEntregaRelatorio[r:Relatorio, c,c':ConselhoPedagogico]{
	one rel:c'.relatorios | {
		rel.analise_resultados = r.analise_resultados &&
		rel.sugestoes = r.sugestoes
	}
	#(c'.relatorios) = #(c.relatorios)
}


pred InvProvaOral[po: ProvaOral]{
	#(po.docentes)>=2
}


pred AprovadoInscrito[a:Aluno]{
	a.aprovado in (a.inscricoes_passadas + a.inscricoes.ECTS)
}


pred EntregaCopia[d:Docente,u:UnidadeCurricular,o,o':OrgaoCompetente]{
	d = u.responsavel
	o.fichas in o'.fichas
	//Quest�o t�cnica - IsoMorfismo 
	one ficha: o'.fichas | {
		ficha.horas_contacto = ~(u.ficha_funcionamento).d.horas_contacto &&
		ficha.resumo = ~(u.ficha_funcionamento).d.resumo &&
		ficha.precedencias = ~(u.ficha_funcionamento).d.precedencias &&
		ficha.competencia_progr = ~(u.ficha_funcionamento).d.competencia_progr &&
		ficha.metodos_ensino = ~(u.ficha_funcionamento).d.metodos_ensino &&
		ficha.bibliografia_basica = ~(u.ficha_funcionamento).d.bibliografia_basica
	}
	#(o'.fichas)=#(o.fichas)+1
}


pred ECTSAnuais[a: Aluno]{
	#(~(a.inscricoes).(UnidadeCurricular - a.inscricoes_passadas))<=60
	#(~(a.inscricoes).(a.inscricoes_passadas))<=18
}


pred RevisaoProva[p:ProvaAvaliacao]{
	some p.juri
}


pred InvPlanoCurso[p: PlanoCurso]{
	#(p.creditos)>=18
}


pred AprovacaoCorrecta[a:Aluno]{
	all u:a.aprovado | #(~(a.avaliacao).u.nota) >=10
}


